Termination proof of /tmp/tmp0d9c1S/LengthOfFiniteLists

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set

↳ CSR

  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

The replacement map contains the following entries:

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length, U42¹, U52¹, LENGTH, U11¹, U21¹, U31¹} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U41¹, U51¹, U62¹, U61¹} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATILIST, ISNATLIST, ISNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

U41¹(tt, V2) → U42¹(isNatIList(V2))
U41¹(tt, V2) → ISNATILIST(V2)
U51¹(tt, V2) → U52¹(isNatList(V2))
U51¹(tt, V2) → ISNATLIST(V2)
U61¹(tt, L, N) → U62¹(isNat(N), L)
U61¹(tt, L, N) → ISNAT(N)
U62¹(tt, L) → LENGTH(L)
ISNAT(length(V1)) → U11¹(isNatList(V1))
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → U21¹(isNat(V1))
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(V) → U31¹(isNatList(V))
ISNATILIST(V) → ISNATLIST(V)
ISNATILIST(cons(V1, V2)) → U41¹(isNat(V1), V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → U51¹(isNat(V1), V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
LENGTH(cons(N, L)) → U61¹(isNatList(L), L, N)
LENGTH(cons(N, L)) → ISNATLIST(L)

The collapsing dependency pairs are DP_c:

U62¹(tt, L) → L

The hidden terms of R are:

zeros

Every hiding context is built from:none

Hence, the new unhiding pairs DP_u are :

U62¹(tt, L) → U(L)
U(zeros) → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 11 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSUsableRulesProof

          ↳ QCSDP

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U51¹} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → U51¹(isNat(V1), V2)
U51¹(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U31(tt) → tt
U41(tt, x0) → U42(isNatIList(x0))
U42(tt) → tt
U61(tt, x0, x1) → U62(isNat(x1), x0)
U62(tt, x0) → s(length(x0))
isNatIList(x0) → U31(isNatList(x0))
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → U41(isNat(x0), x1)
length(nil) → 0
length(cons(x0, x1)) → U61(isNatList(x1), x1, x0)

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSUsableRulesProof

              ↳ QCSDP

                ↳ QCSDPReductionPairProof

          ↳ QCSDP

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52} are replacing on all positions.
For all symbols f in {cons, U51, U51¹} we have µ(f) = {1}.
The symbols in {isNat, isNatList, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → U51¹(isNat(V1), V2)
U51¹(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 1
POL(ISNAT(x₁)) = 2 + x₁
POL(ISNATLIST(x₁)) = 1 + 2·x₁
POL(U11(x₁)) = x₁
POL(U21(x₁)) = 2·x₁
POL(U51(x₁, x₂)) = 2 + 2·x₁
POL(U51¹(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(U52(x₁)) = 2
POL(cons(x₁, x₂)) = 2 + 2·x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = 2 + 2·x₁
POL(nil) = 2
POL(s(x₁)) = 1 + 2·x₁
POL(tt) = 1

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
U11(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U21(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATLIST(cons(V1, V2)) → U51¹(isNat(V1), V2)
U51¹(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)

could be oriented strictly and thus removed.
All pairs have been removed.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSUsableRulesProof

              ↳ QCSDP

                ↳ QCSDPReductionPairProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

          ↳ QCSDP

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52} are replacing on all positions.
For all symbols f in {cons, U51} we have µ(f) = {1}.
The symbols in {isNat, isNatList} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U62¹, U61¹} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

U61¹(tt, L, N) → U62¹(isNat(N), L)
U62¹(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U61¹(isNatList(L), L, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTH(x₁)) = 2·x₁
POL(U11(x₁)) = 2
POL(U21(x₁)) = 2
POL(U51(x₁, x₂)) = 2·x₂
POL(U52(x₁)) = 2·x₁
POL(U61(x₁, x₂, x₃)) = 2 + x₁ + 2·x₂
POL(U61¹(x₁, x₂, x₃)) = 2·x₁ + 2·x₂
POL(U62(x₁, x₂)) = 1 + x₂
POL(U62¹(x₁, x₂)) = 2 + 2·x₂
POL(cons(x₁, x₂)) = 2·x₂
POL(isNat(x₁)) = 2
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = 2 + 2·x₁
POL(nil) = 2
POL(s(x₁)) = 1
POL(tt) = 2
POL(zeros) = 0

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt
U21(tt) → tt
zeros → cons(0, zeros)

could all be oriented weakly.
Furthermore, the pairs

U61¹(tt, L, N) → U62¹(isNat(N), L)
U62¹(tt, L) → LENGTH(L)

could be oriented strictly and thus removed.
The pairs

LENGTH(cons(N, L)) → U61¹(isNatList(L), L, N)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U61¹} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U61¹(isNatList(L), L, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSUsableRulesProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U41¹} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → U41¹(isNat(V1), V2)
U41¹(tt, V2) → ISNATILIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U31(tt) → tt
U41(tt, x0) → U42(isNatIList(x0))
U42(tt) → tt
U61(tt, x0, x1) → U62(isNat(x1), x0)
U62(tt, x0) → s(length(x0))
isNatIList(x0) → U31(isNatList(x0))
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → U41(isNat(x0), x1)
length(nil) → 0
length(cons(x0, x1)) → U61(isNatList(x1), x1, x0)

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSUsableRulesProof

              ↳ QCSDP

                ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52} are replacing on all positions.
For all symbols f in {cons, U51, U41¹} we have µ(f) = {1}.
The symbols in {isNat, isNatList, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → U41¹(isNat(V1), V2)
U41¹(tt, V2) → ISNATILIST(V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 2
POL(ISNATILIST(x₁)) = 1 + 2·x₁
POL(U11(x₁)) = 1 + x₁
POL(U21(x₁)) = 1 + 2·x₁
POL(U41¹(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(U51(x₁, x₂)) = 1 + 2·x₂
POL(U52(x₁)) = 1 + 2·x₁
POL(cons(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = 2 + 2·x₁
POL(nil) = 2
POL(s(x₁)) = 1 + 2·x₁
POL(tt) = 2

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
U11(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U21(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATILIST(cons(V1, V2)) → U41¹(isNat(V1), V2)
U41¹(tt, V2) → ISNATILIST(V2)

could be oriented strictly and thus removed.
All pairs have been removed.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSUsableRulesProof

              ↳ QCSDP

                ↳ QCSDPReductionPairProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.